Inference at * 
Iof proof for Lemma p-mu-exists:


  P:(). Dec(n:. ((P(n))))  (x: + Top. p-mu(P;x)) 

latex

 by ((Auto) 
CollapseTHEN (D (-1))) 

latex

C1: 

C1: 1. P : 
C1: 2. n:. ((P(n)))
C1:   x: + Top. p-mu(P;x)
C2: 

C2: 1. P : 
C2: 2. (n:. ((P(n))))
C2:   x: + Top. p-mu(P;x)
C.

Definitions	P  Q, p-mu(P;x), Top, x:A. B(x), x:A  B(x), , b, x:A. B(x), f(a), Type, x:AB(x), , , t  T, s = t, Dec(P), P  Q, left + right
Lemmas	p-mu wf, top wf, decidable wf, assert wf, nat wf, bool wf